STRATEGY =
(LAMBDA (X) (AND (SUPPORT X))) 
SUPPORT-SET-IS: 
LE(THM37,THM38) 
UNIT-PREFERENCE =NIL
MERGE =NIL
ORDER =NIL
ANCESTRY =T
DEPTH-BOUND =2
LENGTH-BOUND =2

PARMODULATE =T
EQUAL-SYMBOL =R
PAR-DEPTH-BOUND =3
ELAPSED-TIME =42032

NIL 1 2
1 ¬LE(D(D(THM39,THM37),THM38),D(THM39,THM37)) 3 4
2 LE(D(X1,X2),X1) AXIOM 3
3 LE(D(X1,THM38),X2) ¬LE(D(D(X1,THM37),THM38),X2) 5 6
4 ¬LE(D(THM39,THM38),D(THM39,THM37)) AXIOM -12
5 LE(D(X1,THM38),D(D(X1,THM37),THM38)) 7 8
6 LE(X1,X2) ¬LE(X3,X2) ¬LE(X1,X3) AXIOM 9
7 R(D(THM37,THM38),O) 9 10
8 LE(D(D(X1,X2),D(X3,X2)),D(D(X1,X3),X2)) AXIOM 4
9 R(D(X1,X2),O) ¬LE(X1,X2) AXIOM 1
10 LE(THM37,THM38) AXIOM -13